DROPS

Document

DOI: 10.4230/OASIcs.WCET.2022.3

DELOOP: Automatic Flow Facts Computation Using Dynamic Symbolic Execution

Authors: Hazem Abaza, Zain Alabedin Haj Hammadeh, and Daniel Lüdtke

Published in: OASIcs, Volume 103, 20th International Workshop on Worst-Case Execution Time Analysis (WCET 2022)

Abstract

Constructing a complete control-flow graph (CGF) and computing upper bounds on loops of a computing system are essential to safely estimate the worst-case execution time (WCET) of real-time tasks. WCETs are required for verifying the timing requirements of a real-time computing system. Therefore, we propose an analysis using dynamic symbolic execution (DSE) that detects and computes upper bounds on the loops, and resolves indirect jumps. The proposed analysis constructs and initializes memory models, then it uses a satisfiability modulo theories (SMT) solver to symbolically execute the instructions. The analysis showed higher precision in bounding loops of the Mälardalen benchmarks comparing to SWEET and oRange. We integrated our analysis with the OTAWA toolbox for performing a WCET analysis. Then, we used the proposed analysis for estimating the WCET of functions in a use case inspired by an aerospace project.

Cite as

Hazem Abaza, Zain Alabedin Haj Hammadeh, and Daniel Lüdtke. DELOOP: Automatic Flow Facts Computation Using Dynamic Symbolic Execution. In 20th International Workshop on Worst-Case Execution Time Analysis (WCET 2022). Open Access Series in Informatics (OASIcs), Volume 103, pp. 3:1-3:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{abaza_et_al:OASIcs.WCET.2022.3,
  author =	{Abaza, Hazem and Haj Hammadeh, Zain Alabedin and L\"{u}dtke, Daniel},
  title =	{{DELOOP: Automatic Flow Facts Computation Using Dynamic Symbolic Execution}},
  booktitle =	{20th International Workshop on Worst-Case Execution Time Analysis (WCET 2022)},
  pages =	{3:1--3:12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-244-0},
  ISSN =	{2190-6807},
  year =	{2022},
  volume =	{103},
  editor =	{Ballabriga, Cl\'{e}ment},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2022.3},
  URN =		{urn:nbn:de:0030-drops-166256},
  doi =		{10.4230/OASIcs.WCET.2022.3},
  annote =	{Keywords: Real-Time, WCET, Symbolic execution}
}

Search Results

Documents authored by Haj Hammadeh, Zain Alabedin

DELOOP: Automatic Flow Facts Computation Using Dynamic Symbolic Execution

Abstract

Cite as

Thanks for your feedback!

Could not send message